a,b,c:rationals. (a + (b + c)) = ((a + b) + c)  rationals 

latex

Definitions	t  T, imon{i:l}, t.2, t.1, prop{i:l}, P  Q, mon{i:l}, grp{i:l}, abgrp{i:l}, qadd_grp, grp_op(g), x f y, grp_car(g), x:A. B(x)
Lemmas	abgrp wf, grp id wf, grp op wf, grp car wf, monoid p wf, qadd grp wf, mon assoc